Nuprl Definition : init_p 11,40

init_p(es; i; T; x; v) == subtype_rel(es-vartype(es; i; x); T) c (es_init(es)(i,x) = v) 
latex



clarification:

init_p(es; i; T; x; v)
== subtype_rel(es-vartype(es; i; x); T) c (es_init(es)(i,x) = v  rationalsT) 
latex


DefinitionsA c B, es-vartype(es; i; x), s = t, x:AB(x), rationals, f(a), es_init(es)
FDL editor aliasesinit_p

origin